io.Read_Handler.read

(max_count i32)

[Abstract feature]

read up to count bytes

returns either an array of the bytes read, end_of_file or an error

Postcondition

post debug: (result ? s Sequence => s.count<=max_count | * => true)
     debug 10 : (result ? s Sequence => s.is_array_backed | * => true)

0.097dev (GIT hash 6a5de4939ddf29875c1d9a706508d9bfd0cd7ca9)

last changed: 2026-06-09